D:Dsys, i:Id. {m:M(i).Msg| source(mlnk(m)) = i }  Msg(l,tg. M(source(l)).dout(l,tg)) 

latex

Definitions	t  T, IdLnk, x:A. B(x), source(l), M(i), M.dout(l,tg), Id, Msg(M), mlnk(m), M.Msg, Dsys, Msg(da)
Lemmas	subtype rel self, Id wf, dsys wf, ma-msg wf, mlnk wf d, Msg wf, ma-dout wf, d-m wf, lsrc wf, IdLnk wf